Nuprl Definition : bframe-p
0,22
postcript
pdf
@
i
:
k
sends only on links in
L
==
e
@
i
. kind(
e
) =
k
(
l
:IdLnk.
(
l
L
)
sends(
l
;
e
) = nil)
latex
clarification:
bframe-p(
es
;
i
;
k
;
L
)
== alle-at(
es
;
i
;
e
.es-kind(
es
;
e
) =
k
Knd
== alle-at(
es
;
i
;
e
.
(
l
:IdLnk.
== alle-at(
es
;
i
;
e
.
(
(
l
L
IdLnk)
es-sends(
es
;
l
;
e
) = nil
es-Msg(
es
) List))
latex
Definitions
e
@
i
.
P
(
e
)
,
Knd
,
kind(
e
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
A
,
(
x
l
)
,
IdLnk
,
s
=
t
,
type
List
,
Msg
,
sends(
l
;
e
)
,
nil
FDL editor aliases
bframe-p
origin